open HolKernel Parse boolLib bossLib;

(*
quietdec := true;

val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/");
loadPath := (concat home_dir "src/deep_embeddings") ::
            (concat home_dir "src/translations") ::
            (concat home_dir "src/tools") ::
            (concat hol_dir "examples/PSL/path") ::
            (concat hol_dir "examples/PSL/1.1/official-semantics") :: !loadPath;

map load
 ["full_ltlTheory", "arithmeticTheory", "automaton_formulaTheory", "xprop_logicTheory", "prop_logicTheory",
  "infinite_pathTheory", "tuerk_tacticsLib", "symbolic_semi_automatonTheory", "listTheory", "pred_setTheory",
  "pred_setTheory", "rich_listTheory", "set_lemmataTheory", "temporal_deep_mixedTheory",
  "pairTheory", "symbolic_kripke_structureTheory",
  "numLib", "semi_automatonTheory", "omega_automatonTheory",
  "omega_automaton_translationsTheory", "ctl_starTheory",
  "ltl_to_automaton_formulaTheory", "containerTheory",
  "psl_to_rltlTheory", "rltl_to_ltlTheory", "temporal_deep_simplificationsLib", "congLib",
  "kripke_structureTheory"];
*)

open full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory
     prop_logicTheory
     infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory listTheory pred_setTheory
     pred_setTheory rich_listTheory set_lemmataTheory temporal_deep_mixedTheory pairTheory symbolic_kripke_structureTheory
     numLib semi_automatonTheory omega_automatonTheory
     omega_automaton_translationsTheory ctl_starTheory
     ltl_to_automaton_formulaTheory containerTheory
     psl_to_rltlTheory rltl_to_ltlTheory temporal_deep_simplificationsLib congLib kripke_structureTheory;
open Sanity;

val _ = hide "K";
val _ = hide "S";
val _ = hide "I";


(*
show_assums := false;
show_assums := true;
show_types := true;
show_types := false;
quietdec := false;
*)


val _ = new_theory "ibm";


val A_UNIV___LTL_KS_SEM___CONCRETE_THM =
  store_thm (
    "A_UNIV___LTL_KS_SEM___CONCRETE_THM",
    ``!A ac l. (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l)) ==>
    (!i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==>

          (((A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = LTL_SEM i l) =
      LTL_SEM (INPUT_RUN_PATH_UNION A i w) (LTL_EQUIV (ACCEPT_COND_TO_LTL ac, l)))))``,


  REPEAT STRIP_TAC THEN
  SIMP_TAC std_ss [A_SEM_THM,
    SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___INITIAL_PATH] THEN
  `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w` by
    PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN
  SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN
  WEAKEN_HD_TAC THEN
  `(!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==>
          ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac) =
      ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac` by METIS_TAC[] THEN
  ASM_SIMP_TAC std_ss [LTL_SEM_THM, ACCEPT_COND_TO_LTL_THM] THEN

  MATCH_MP_TAC (prove (``(A = C) ==> ((B = A) = (B = C))``, PROVE_TAC[])) THEN

  ONCE_REWRITE_TAC[LTL_USED_VARS_INTER_THM] THEN
  AP_THM_TAC THEN AP_TERM_TAC THEN
  ONCE_REWRITE_TAC [FUN_EQ_THM] THEN GEN_TAC THEN
  UNDISCH_NO_TAC 3 (*DISJOINT A.S (LTL_USED_VARS l)*) THEN
  `PATH_SUBSET w A.S` by FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN
  UNDISCH_HD_TAC THEN
  REPEAT WEAKEN_HD_TAC THEN
  SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, DISJOINT_DISJ_THM,
    INPUT_RUN_PATH_UNION_def, EXTENSION, INPUT_RUN_STATE_UNION_def,
    IN_UNION, IN_INTER, IN_DIFF, PATH_SUBSET_def, SUBSET_DEF] THEN
  METIS_TAC[]
);




val A_UNIV___A_SEM___CONCRETE_THM =
  store_thm (
    "A_UNIV___A_SEM___CONCRETE_THM",
    ``!A ac (l:'a ltl). (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l) /\ FINITE A.S /\ INFINITE (UNIV:'a set)) ==>

    (?A' fc p. FINITE A'.S /\
    (!i.
          (((A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = LTL_SEM i l) =
            (A_SEM i (A_UNIV (A',
            A_IMPL(A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc),
                   ACCEPT_COND_PROP p))))))))``,


  REPEAT STRIP_TAC THEN
  ASSUME_TAC A_UNIV___LTL_KS_SEM___CONCRETE_THM THEN
  Q_SPECL_NO_ASSUM 0 [`A`, `ac`, `l`] THEN
  PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN
  ASM_SIMP_TAC std_ss [] THEN

  `?pf DS. (pf, DS) = LTL_TO_GEN_BUECHI (LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l)) F T` by METIS_TAC[PAIR] THEN

  `?UV. UV = (P_USED_VARS A.S0 UNION XP_USED_VARS A.R UNION
           (ACCEPT_COND_USED_VARS ac) UNION LTL_USED_VARS l UNION A.S)` by METIS_TAC[] THEN
  SUBGOAL_TAC `DS.IV SUBSET UV` THEN1 (
    `DS.IV = LTL_USED_VARS (LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l))` by METIS_TAC[LTL_TO_GEN_BUECHI___USED_INPUT_VARS, SND] THEN
    ASM_SIMP_TAC std_ss [SUBSET_DEF, LTL_USED_VARS_EVAL,
      LTL_USED_VARS___ACCEPT_COND_TO_LTL, DISJOINT_DISJ_THM,
      IN_UNION] THEN
    PROVE_TAC[]
  ) THEN

  SUBGOAL_TAC `FINITE UV` THEN1 (
    ASM_SIMP_TAC std_ss [FINITE_UNION,
      FINITE___P_USED_VARS, FINITE___XP_USED_VARS, FINITE___LTL_USED_VARS,
      FINITE___ACCEPT_COND_USED_VARS]
  ) THEN
  `?sv. IS_ELEMENT_ITERATOR sv DS.SN UV` by METIS_TAC[IS_ELEMENT_ITERATOR_EXISTS] THEN

  ASSUME_TAC LTL_TO_GEN_BUECHI_DS___SEM___MIN THEN
  Q_SPECL_NO_ASSUM 0 [`DS`, `LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l)`, `pf`, `sv`, `F`] THEN
  PROVE_CONDITION_NO_ASSUM 0 THEN1 (
    REPEAT STRIP_TAC THENL [
      ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def] THEN
      PROVE_TAC[IS_ELEMENT_ITERATOR_SUBSET],

      METIS_TAC[LTL_TO_GEN_BUECHI_THM, SND, FST],
      METIS_TAC[LTL_TO_GEN_BUECHI_THM, SND, FST]
    ]
  ) THEN
  FULL_SIMP_TAC std_ss [] THEN
  WEAKEN_HD_TAC THEN


  SIMP_ALL_TAC std_ss [LTL_TO_GEN_BUECHI_DS___A_UNIV_def,
    LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def] THEN
  Q.ABBREV_TAC `B = (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv)` THEN
  Q_TAC EXISTS_TAC `PRODUCT_SEMI_AUTOMATON A B` THEN
  Q_TAC EXISTS_TAC `MAP (\x. x sv) DS.FC` THEN
  Q_TAC EXISTS_TAC `pf sv` THEN
  REPEAT STRIP_TAC THENL [
    Q.UNABBREV_TAC `B` THEN
    ASM_SIMP_TAC std_ss [PRODUCT_SEMI_AUTOMATON_REWRITES, FINITE_UNION,
      LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS___FINITE],


    `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w` by
      PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN
    SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN
    Q_SPECL_NO_ASSUM 8 [`i`, `w`] THEN
    PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN
    ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN

    SIMP_TAC std_ss [MAP_MAP_o, combinTheory.o_DEF] THEN

    ASSUME_TAC (SIMP_RULE std_ss [RIGHT_FORALL_IMP_THM] (GSYM TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_PRODUCT_THM)) THEN
    Q_SPECL_NO_ASSUM 0 [`A`, `B`, `i`, `w`] THEN
    PROVE_CONDITION_NO_ASSUM 0 THEN1 (
      Q.UNABBREV_TAC `B` THEN
      ASM_SIMP_TAC std_ss [DISJOINT_DISJ_THM,
        SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION,
        LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def,
        symbolic_semi_automaton_REWRITES,
        LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def,
        IN_ABS] THEN
      SIMP_ALL_TAC std_ss [IS_ELEMENT_ITERATOR_def] THEN
      GEN_TAC THEN
      RIGHT_DISJ_TAC THEN
      SIMP_ALL_TAC std_ss [] THEN
      `~(x IN UV)` by METIS_TAC[] THEN
      UNDISCH_HD_TAC THEN
      ASM_SIMP_TAC std_ss [IN_UNION]
    ) THEN
    ASM_SIMP_TAC std_ss []
  ]
);








val IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS =
  store_thm (
    "IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS",

``!A p (l:'a ltl). INFINITE (UNIV:'a set) /\ FINITE A.S ==>

((!K. (A_KS_SEM K (A_UNIV (A, ACCEPT_COND_G p)) = LTL_KS_SEM K l)) =
(!i. A_SEM i (A_UNIV (A, ACCEPT_COND_G p)) = LTL_SEM i l))``,


REPEAT STRIP_TAC THEN EQ_TAC THENL [
  ALL_TAC,
  SIMP_TAC std_ss [A_KS_SEM_def, LTL_KS_SEM_def]
] THEN

REPEAT STRIP_TAC THEN
CCONTR_TAC THEN
REMAINS_TAC `?i'. IS_ULTIMATIVELY_PERIODIC_PATH i' /\
                  ~(A_SEM i' (A_UNIV (A,ACCEPT_COND_G p)) = LTL_SEM i' l)` THEN1 (

  `?V. V = SEMI_AUTOMATON_USED_INPUT_VARS A UNION (P_USED_VARS p DIFF A.S) UNION LTL_USED_VARS l` by METIS_TAC[] THEN

  ASSUME_TAC ULTIMALTIVELY_PERIODIC_PATH_CORRESPONDING_TO_UNIQUE_PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURES THEN
  Q_SPECL_NO_ASSUM 0 [`i'`, `V`] THEN
  PROVE_CONDITION_NO_ASSUM 0 THEN1 (
    ASM_SIMP_TAC std_ss [FINITE_UNION,
      FINITE___LTL_USED_VARS,
      FINITE___SEMI_AUTOMATON_USED_INPUT_VARS,
      FINITE___P_USED_VARS, FINITE_DIFF]
  ) THEN
  CLEAN_ASSUMPTIONS_TAC THEN

  SUBGOAL_TAC `!i. LTL_SEM i l = LTL_SEM (PATH_RESTRICT i V) l` THEN1 (
    SIMP_TAC std_ss [LTL_SEM_def] THEN
    METIS_TAC[LTL_USED_VARS_INTER_SUBSET_THM, SUBSET_UNION]
  ) THEN

  SUBGOAL_TAC `!i. A_SEM i (A_UNIV (A,ACCEPT_COND_G p)) = A_SEM (PATH_RESTRICT i V) (A_UNIV (A,ACCEPT_COND_G p))` THEN1 (
    MATCH_MP_TAC A_USED_INPUT_VARS_INTER_SUBSET_THM THEN
    ASM_SIMP_TAC std_ss [A_USED_INPUT_VARS_def, A_UNIV_def,
      ACCEPT_COND_G_def, ACCEPT_COND_USED_VARS_def, SUBSET_DEF,
      IN_UNION]
  ) THEN

  Q_SPEC_NO_ASSUM 8 `M` THEN
  UNDISCH_HD_TAC THEN
  SIMP_TAC std_ss [A_KS_SEM_def, LTL_KS_SEM_def] THEN
  METIS_TAC[]
) THEN
WEAKEN_NO_TAC 1 (*clean up LTL_KS_SEM M ...*) THEN

ASSUME_TAC SYMBOLIC___UNIV_G___TO___DET_GF___EXISTS_THM THEN
Q_SPECL_NO_ASSUM 0 [`LTL_USED_VARS l`, `A`, `p`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[FINITE___LTL_USED_VARS] THEN
CLEAN_ASSUMPTIONS_TAC THEN
FULL_SIMP_TAC std_ss [ACCEPT_COND_GF_def] THEN
WEAKEN_NO_TAC 4 THEN


ASSUME_TAC A_UNIV___A_SEM___CONCRETE_THM THEN
Q_SPECL_NO_ASSUM 0 [`A'`, `ACCEPT_G (ACCEPT_F (ACCEPT_PROP p'))`, `l`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN

FULL_SIMP_TAC std_ss [] THEN
FULL_SIMP_TAC std_ss [] THEN
WEAKEN_HD_TAC THEN

SUBGOAL_TAC `?B fc' p'. FINITE B.S /\
                        IS_SIMPLE_SYMBOLIC_SEMI_AUTOMATON B /\
                        (!i. A_SEM i
                              (A_UNIV
                                (A'',
                                  A_IMPL
                                    (A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc),
                                    ACCEPT_COND_PROP p))) =
                             A_SEM i
                              (A_UNIV
                                (B,
                                  A_IMPL
                                    (A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc'),
                                    ACCEPT_COND_PROP p'))))` THEN1 (


  SUBGOAL_TAC `!i A fc p. A_SEM i (A_UNIV (A, A_IMPL
                                  (A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc),
                                  ACCEPT_COND_PROP p))) =
                          A_SEM i (A_UNIV (A, ACCEPT_COND (ACCEPT_IMPL
                                  (ACCEPT_BIGAND (MAP (\x. ACCEPT_G (ACCEPT_F (ACCEPT_PROP x))) fc),
                                  ACCEPT_PROP p))))` THEN1 (
    ASM_SIMP_TAC std_ss [A_SEM_THM, A_BIGAND_SEM, MEM_MAP,
      GSYM LEFT_FORALL_IMP_THM, ACCEPT_COND_GF_def, A_SEM_def,
      ACCEPT_COND_SEM_def, ACCEPT_COND_PROP_def,
      ACCEPT_IMPL_def, ACCEPT_OR_def, ACCEPT_COND_SEM_TIME_def,
      ACCEPT_BIGAND_SEM] THEN
    METIS_TAC[]
  ) THEN
  ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN

  Q.ABBREV_TAC `ac = (ACCEPT_IMPL
                        (ACCEPT_BIGAND
                           (MAP (\x. ACCEPT_G (ACCEPT_F (ACCEPT_PROP x)))
                              fc),ACCEPT_PROP p))` THEN
  SUBGOAL_TAC `?f. INJ f (SEMI_AUTOMATON_USED_INPUT_VARS A'') UNIV /\
       DISJOINT (IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A'') )
                (SEMI_AUTOMATON_USED_VARS A'' UNION ACCEPT_COND_USED_VARS ac)` THEN1 (
    MATCH_MP_TAC (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] FINITE_INJ_EXISTS) THEN
    ASM_SIMP_TAC std_ss [FINITE___SEMI_AUTOMATON_USED_INPUT_VARS,
                         FINITE_UNION, SEMI_AUTOMATON_USED_VARS_def,
                         FINITE___ACCEPT_COND_USED_VARS]
  ) THEN

  SUBGOAL_TAC `?SA. IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON SA A'' f` THEN1 (
    FULL_SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_UNION, IN_IMAGE,
      SEMI_AUTOMATON_USED_VARS_def, IN_DIFF, IN_SING,
      IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def] THEN
    REPEAT STRIP_TAC THENL [
      METIS_TAC[],
      METIS_TAC[],
      FULL_SIMP_TAC std_ss [INJ_DEF, IN_UNIV] THEN  METIS_TAC[]
    ]
  ) THEN

  ASSUME_TAC A_UNIV___SIMPLIFIED_SEMI_AUTOMATON_THM THEN
  Q_SPECL_NO_ASSUM 0 [`A''`, `SA`, `f`, `ac`] THEN
  PROVE_CONDITION_NO_ASSUM 0 THEN1 (
    FULL_SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_UNION, IN_IMAGE,
      SEMI_AUTOMATON_USED_VARS_def, IN_DIFF, IN_SING] THEN
    METIS_TAC[]
  ) THEN

  ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN
  Q.UNABBREV_TAC `ac` THEN
  SIMP_TAC std_ss [ACCEPT_VAR_RENAMING_def, ACCEPT_IMPL_def,
    ACCEPT_OR_def, ACCEPT_BIGAND___VAR_RENAMING, MAP_MAP_o,
    combinTheory.o_DEF, ACCEPT_F_def] THEN
  Q_TAC EXISTS_TAC `SA` THEN
  Q_TAC EXISTS_TAC `MAP (P_VAR_RENAMING
    (\x. (if x IN SEMI_AUTOMATON_USED_INPUT_VARS A'' then f x else x))) fc` THEN
  Q_TAC EXISTS_TAC `P_VAR_RENAMING
    (\x. (if x IN SEMI_AUTOMATON_USED_INPUT_VARS A'' then f x else x)) p` THEN
  REPEAT STRIP_TAC THENL [
    SIMP_ALL_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def] THEN
    ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES,
      FINITE_UNION, IMAGE_FINITE, FINITE___SEMI_AUTOMATON_USED_INPUT_VARS],

    METIS_TAC[IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUNS],

    SIMP_TAC std_ss [MAP_MAP_o, combinTheory.o_DEF]
  ]
) THEN
FULL_SIMP_TAC std_ss [] THEN

(*cleanup*)
WEAKEN_HD_TAC THEN
WEAKEN_NO_TAC 2 (*FINITE A''.S*) THEN
NTAC 4 (WEAKEN_NO_TAC 2) (*A'*) THEN
WEAKEN_NO_TAC 3 (*A*) THEN


FULL_SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_PROP_def, ACCEPT_COND_SEM_def,
  ACCEPT_COND_SEM_TIME_def, A_BIGAND_SEM, MEM_MAP,
  GSYM LEFT_FORALL_IMP_THM, ACCEPT_COND_GF_def, ACCEPT_F_def,
  IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_def,
  IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_THM] THEN

SUBGOAL_TAC `?e. !n:num. ?m:num. m > n /\ (w m = e)` THEN1 (
  ASSUME_TAC (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] (INST_TYPE [alpha |-> alpha --> bool] INF_ELEMENTS_OF_PATH_NOT_EMPTY)) THEN
  Q_SPECL_NO_ASSUM 0 [`POW B.S`, `w`] THEN
  PROVE_CONDITION_NO_ASSUM 0 THEN1 (
    FULL_SIMP_TAC std_ss [PATH_SUBSET_def, IN_POW, FINITE_POW_IFF]
  ) THEN
  FULL_SIMP_TAC std_ss [GSYM MEMBER_NOT_EMPTY,
    INF_ELEMENTS_OF_PATH_def, GSPECIFICATION] THEN
  METIS_TAC[]
) THEN

`?n0. w n0 = e` by METIS_TAC[] THEN

SUBGOAL_TAC `?m':num. (m' > n0) /\
              (!x. MEM x fc' ==> ?t. n0 <= t /\ t < m' /\
                   P_SEM (INPUT_RUN_PATH_UNION B i w t) x)` THEN1 (
  Induct_on `fc'` THENL [
    SIMP_TAC list_ss [] THEN
    Q_TAC EXISTS_TAC `SUC n0` THEN
    DECIDE_TAC,

    SIMP_TAC list_ss [DISJ_IMP_THM, FORALL_AND_THM] THEN
    REPEAT STRIP_TAC THEN
    PROVE_CONDITION_NO_ASSUM 2 THEN1 ASM_REWRITE_TAC[] THEN
    Q_SPEC_NO_ASSUM 2 `n0` THEN
    FULL_SIMP_TAC std_ss [] THEN
    rename1 `P_SEM (INPUT_RUN_PATH_UNION B i w t2) h` THEN
    Q_TAC EXISTS_TAC `MAX m' (SUC t2)` THEN

    ASM_SIMP_TAC arith_ss [GREATER_DEF, MAX_LT] THEN
    REPEAT STRIP_TAC THENL [
      Q_TAC EXISTS_TAC `t2` THEN
      ASM_SIMP_TAC arith_ss [],

      METIS_TAC[]
    ]
  ]
) THEN
SUBGOAL_TAC `?m. (m + n0) >= m' /\ (w (m + n0) = e)` THEN1 (
  Q_SPEC_NO_ASSUM 3 `m'` THEN
  CLEAN_ASSUMPTIONS_TAC THEN
  Q_TAC EXISTS_TAC `m - n0` THEN
  ASM_SIMP_TAC arith_ss []
) THEN

Q_TAC EXISTS_TAC `CUT_PATH_PERIODICALLY i n0 m` THEN
STRIP_TAC THEN1 (
  REWRITE_TAC[IS_ULTIMATIVELY_PERIODIC_PATH_def] THEN
  Q_TAC EXISTS_TAC `n0` THEN
  Q_TAC EXISTS_TAC `m` THEN
  ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___IS_ULTIMATIVELY_PERIODIC]
) THEN

Q_TAC EXISTS_TAC `CUT_PATH_PERIODICALLY w n0 m` THEN
REPEAT STRIP_TAC THENL [
  SIMP_ALL_TAC std_ss [PATH_SUBSET_def, CUT_PATH_PERIODICALLY_def] THEN
  METIS_TAC[],


  FULL_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___BEGINNING,
    INPUT_RUN_PATH_UNION_def],

  Cases_on `SUC n < m + n0` THEN1 (
    ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___BEGINNING]
  ) THEN
  ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY_def] THEN
  Cases_on `m = 1` THEN1 (
    ASM_SIMP_TAC std_ss [MOD_1] THEN
    `m + n0 = SUC n0` by DECIDE_TAC THEN
    METIS_TAC[]
  ) THEN
  SUBGOAL_TAC `(SUC n - n0) MOD m = (1 + (n - n0) MOD m) MOD m` THEN1 (
    SUBGOAL_TAC `1 MOD m = 1` THEN1 (
      MATCH_RIGHT_EQ_MP_TAC X_MOD_Y_EQ_X THEN
      DECIDE_TAC
    ) THEN
    GSYM_NO_TAC 0 THEN ONCE_ASM_REWRITE_TAC [] THEN WEAKEN_HD_TAC THEN

    ASM_SIMP_TAC arith_ss [MOD_PLUS] THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN
    DECIDE_TAC
  ) THEN
  ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN
  Q.ABBREV_TAC `r = (n - n0) MOD m` THEN
  Cases_on `1 + r < m` THENL [
    ASM_SIMP_TAC arith_ss [] THEN
    `n0 + (r + 1) = SUC (n0 + r)` by DECIDE_TAC THEN
    METIS_TAC[],

    SUBGOAL_TAC `1 + r = m` THEN1 (
      `0 < m` by DECIDE_TAC THEN
      `r < m` by METIS_TAC [DIVISION] THEN
      DECIDE_TAC
    ) THEN
    ASM_SIMP_TAC arith_ss [] THEN

    `SUC (n0 + r) = (m + n0)` by DECIDE_TAC THEN
    METIS_TAC[]
  ],

  RES_TAC THEN
  rename1 `(_ >= t') /\ P_SEM _ p` THEN
  Q_TAC EXISTS_TAC `m * t' + t` THEN
  SUBGOAL_TAC `m * t' >= t'` THEN1 (
    `m > 0` by DECIDE_TAC THEN UNDISCH_HD_TAC THEN
    SIMP_TAC arith_ss [GREATER_EQ]
  ) THEN
  ASM_SIMP_TAC arith_ss [] THEN WEAKEN_HD_TAC THEN

  SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def, CUT_PATH_PERIODICALLY_def] THEN
  ASM_SIMP_TAC arith_ss [] THEN
  REMAINS_TAC `(n0 + (t + m * t' - n0) MOD m) = t` THEN1 (
    ASM_REWRITE_TAC[]
  ) THEN
  `(t + m * t' - n0) = ((t - n0) + m * t')` by DECIDE_TAC THEN
  ONCE_ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN
  `0 < m` by DECIDE_TAC THEN

  ASSUME_TAC MOD_MULT THEN
  Q_SPECL_NO_ASSUM 0 [`m`, `t - n0`] THEN
  PROVE_CONDITION_NO_ASSUM 0 THEN1 FULL_SIMP_TAC arith_ss [] THEN
  Q_SPEC_NO_ASSUM 0 `t'` THEN
  UNDISCH_HD_TAC THEN
  SIMP_TAC std_ss [ADD_SYM, MULT_SYM] THEN
  DECIDE_TAC,


  UNDISCH_HD_TAC THEN
  FULL_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___BEGINNING,
    INPUT_RUN_PATH_UNION_def]
]);






val SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___TO___AUTOMATON =
  store_thm (
    "SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___TO___AUTOMATON",

    ``!K A p. (DISJOINT (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS K) A.S) ==>
          ((CTL_KS_SEM (SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K A)
          (CTL_A_ALWAYS (CTL_PROP p))) =
          A_KS_SEM K (A_UNIV (A, ACCEPT_COND_G p)))``,


  SIMP_TAC std_ss [CTL_KS_SEM_def,
    SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT,
    symbolic_kripke_structure_REWRITES, CTL_SEM_THM,
    PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, P_SEM_THM, XP_SEM_THM,
    GSYM RIGHT_FORALL_IMP_THM,
    A_KS_SEM_def, A_SEM_THM, ACCEPT_COND_G_def, ACCEPT_COND_SEM_def,
    ACCEPT_COND_SEM_TIME_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def,
    IS_TRANSITION_def, GSYM SUBSET_COMPL_DISJOINT,
    SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, UNION_SUBSET] THEN
  REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [
    rename1 `P_SEM (INPUT_RUN_PATH_UNION A i w t') p` THEN
    REMAINS_TAC `P_SEM (INPUT_RUN_PATH_UNION A i w 0) K.S0 /\
                !n. XP_SEM K.R (INPUT_RUN_STATE_UNION A (i n) (w n),
                                INPUT_RUN_STATE_UNION A (i (SUC n)) (w (SUC n)))` THEN1 (
      Q_SPECL_NO_ASSUM 7 [`INPUT_RUN_PATH_UNION A i w`, `t'`] THEN
      FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def]
    ) THEN
    SUBGOAL_TAC `!n. (INPUT_RUN_STATE_UNION A (i n) (w n)) INTER (COMPL A.S) =
                    (i n) INTER (COMPL A.S)` THEN1 (
      SIMP_ALL_TAC std_ss [INPUT_RUN_STATE_UNION_def, EXTENSION, IN_INTER, IN_COMPL, IN_UNION, IN_DIFF, PATH_SUBSET_def, PATH_MAP_def, SUBSET_DEF] THEN
      PROVE_TAC[]
    ) THEN
    SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def] THEN
    REPEAT STRIP_TAC THENL [
      METIS_TAC[P_USED_VARS_INTER_SUBSET_THM],
      METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM]
    ],


    Q_SPECL_NO_ASSUM 3 [`p'`, `PATH_RESTRICT p' A.S`, `k`] THEN
    SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def, PATH_RESTRICT_def, PATH_MAP_def,
      INPUT_RUN_STATE_UNION___SPLIT, PATH_SUBSET_def, INTER_SUBSET] THEN
    PROVE_TAC[]
  ]);


val SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___CLEAN_STATE_VARS =
  store_thm (
    "SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___CLEAN_STATE_VARS",

    ``!K A p.
          (CTL_KS_SEM (SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K A)
          (CTL_A_ALWAYS (CTL_PROP p))) =
          (CTL_KS_SEM (SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K (symbolic_semi_automaton EMPTY A.S0 A.R))
          (CTL_A_ALWAYS (CTL_PROP p)))``,

      SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT_def,
        SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def,
        SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, symbolic_kripke_structure_REWRITES,
        symbolic_semi_automaton_REWRITES]
  );



val A_KS_SEM___cong =
  store_thm (
    "A_KS_SEM___cong",
    ``!A1 A2. AUTOMATON_EQUIV A1 A2 ==> !K. (A_KS_SEM K A1 = A_KS_SEM K A2)``,
      SIMP_TAC std_ss [A_KS_SEM_def, AUTOMATON_EQUIV_def]);





val A_UNIV___LTL_KS_SEM___THM =
  store_thm (
    "A_UNIV___LTL_KS_SEM___THM",
    ``!A ac l. (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l)) ==>
    ((!i. A_SEM i (A_UNIV (A, ACCEPT_COND ac)) =
        LTL_SEM i l) =
    LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE A)
      (LTL_EQUIV (ACCEPT_COND_TO_LTL ac, l)))``,


  REPEAT STRIP_TAC THEN
  SIMP_TAC std_ss [LTL_KS_SEM_def, A_SEM_THM,
    SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___INITIAL_PATH] THEN
  EQ_TAC THEN REPEAT STRIP_TAC THENL [
    Q_SPEC_NO_ASSUM 1 `p` THEN
    `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A p w` by
      PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN
    SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN
    `LTL_SEM p l = ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A p (PATH_RESTRICT p A.S)) ac` by METIS_TAC[] THEN
    FULL_SIMP_TAC std_ss [LTL_SEM_THM, ACCEPT_COND_TO_LTL_THM, INPUT_RUN_PATH_UNION___SPLIT],

    `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w` by
      PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN
    SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN
    `(!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==>
          ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac) =
      ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac` by METIS_TAC[] THEN
    ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN
    Q_SPEC_NO_ASSUM 2 `INPUT_RUN_PATH_UNION A i w` THEN
    SUBGOAL_TAC `IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A
                    (INPUT_RUN_PATH_UNION A i w)
                    (PATH_RESTRICT (INPUT_RUN_PATH_UNION A i w) A.S)` THEN1 (
      UNDISCH_NO_TAC 1 THEN
      SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def,
        INPUT_RUN_PATH_UNION_def, PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def,
        INTER_SUBSET, INPUT_RUN_STATE_UNION_def, IS_TRANSITION_def] THEN
      SUBGOAL_TAC `!n. ((w n UNION (i n DIFF A.S)) INTER A.S UNION
                        (w n UNION (i n DIFF A.S) DIFF A.S)) =
                      (w n UNION (i n DIFF A.S))` THEN1 (
        SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_INTER, IN_DIFF] THEN
        METIS_TAC[]
      ) THEN
      ASM_SIMP_TAC std_ss []
    ) THEN
    FULL_SIMP_TAC std_ss [LTL_SEM_THM, GSYM ACCEPT_COND_TO_LTL_THM,
      ACCEPT_COND_SEM_def] THEN
    ONCE_REWRITE_TAC[LTL_USED_VARS_INTER_THM] THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN
    `PATH_SUBSET w A.S` by FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN
    ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
    SIMP_ALL_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, EXTENSION, IN_INTER,
      INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF, PATH_SUBSET_def, SUBSET_DEF, GSYM SUBSET_COMPL_DISJOINT, IN_COMPL] THEN
    METIS_TAC[]
  ]);







val PROBLEM_TO_LTL_KS_SEM =
  store_thm ("PROBLEM_TO_LTL_KS_SEM",
    ``!A p psl i0 s0 f f'. (F_CLOCK_SERE_FREE psl /\
           ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION
             F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\
           (A.S = (INTERVAL_SET (SUC i0) s0)) /\
           (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\
           (i0 <= s0) /\
           (f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)))) /\
           (f' = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)) +  2**(SUC(s0-i0))))) ==>


            ((LTL_KS_SEM
                  (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE
                    (SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON
                        (symbolic_semi_automaton (INTERVAL_SET (SUC i0) (SUC s0))
                          (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0))
                          (XP_AND
                              (XP_EQUIV
                                (XP_NEXT_PROP (SUC s0),
                                  XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),A.R)))
                        f f' (P_PROP (SUC s0))))
                  (LTL_EQUIV (LTL_ALWAYS (LTL_EVENTUAL
                                (LTL_PROP (P_NOT (P_BIGOR (SET_TO_LIST
                                            (IMAGE (\s. P_PROP (f' s))
                                                (POW (INTERVAL_SET (SUC i0) (SUC s0))))))))),
                             PSL_TO_LTL psl))

      )  =

      (!K.
      ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) =
       UF_KS_SEM K psl)))``,



REPEAT STRIP_TAC THEN
ASM_SIMP_TAC std_ss [PSL_TO_LTL___UF_KS_SEM] THEN

ASSUME_TAC (INST_TYPE [alpha |-> num] IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS) THEN
Q_SPECL_NO_ASSUM 0 [`A`,  `p`, `(PSL_TO_LTL psl)`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  ASM_REWRITE_TAC[FINITE_INTERVAL_SET,
  INFINITE_UNIV] THEN
  Q_TAC EXISTS_TAC `SUC` THEN
  SIMP_TAC arith_ss [] THEN
  EXISTS_TAC ``0:num`` THEN
  SIMP_TAC arith_ss []
) THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN


SUBGOAL_TAC `!i. A_SEM i (A_UNIV (A,ACCEPT_COND_G p)) =
             ~A_SEM i (A_NDET (A,ACCEPT_COND_F (P_NOT p)))` THEN1 (
  SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_G_def,
    ACCEPT_COND_F_def, ACCEPT_F_def,
    ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, P_SEM_def] THEN
  PROVE_TAC[]
) THEN
FULL_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN


ASSUME_TAC (INST_TYPE [alpha |-> num] A_SEM___NDET_F___TO___NDET_FG) THEN
Q_SPECL_NO_ASSUM 0 [`A`, `P_NOT p`, `SUC s0`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, P_USED_VARS_def,
    IN_UNION, IN_INTERVAL_SET, SUBSET_DEF] THEN
  `~(SUC s0 <= i0) /\ ~(SUC s0 <= s0)` by DECIDE_TAC THEN
  PROVE_TAC[]
) THEN
SIMP_ALL_TAC std_ss [AUTOMATON_EQUIV_def] THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN


SUBGOAL_TAC `SUC s0 INSERT INTERVAL_SET (SUC i0) s0 =
             INTERVAL_SET (SUC i0) (SUC s0)` THEN1 (
  ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN
  SIMP_TAC std_ss [IN_INTERVAL_SET, IN_INSERT] THEN
  DECIDE_TAC
) THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN



ASSUME_TAC (INST_TYPE [alpha |-> num] SYMBOLIC___NDET_FG___TO___DET_FG___CONCRETE_THM) THEN
Q_SPECL_NO_ASSUM 0 [`symbolic_semi_automaton ((INTERVAL_SET (SUC i0) (SUC s0)))
       (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0))
             (XP_AND
                (XP_EQUIV
                   (XP_NEXT_PROP (SUC s0),
                    XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),A.R))`,
              `P_PROP (SUC s0)`, `f`, `f'`] THEN
SIMP_ALL_TAC std_ss [symbolic_semi_automaton_REWRITES] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  SUBGOAL_TAC `SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)` THEN1 (
    FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, IN_UNION,
      SUBSET_DEF, IN_INTERVAL_SET] THEN
    REPEAT STRIP_TAC THEN
    `x <= i0` by PROVE_TAC[] THEN
    DECIDE_TAC
  ) THEN

  SUBGOAL_TAC `(SEMI_AUTOMATON_USED_VARS
          (symbolic_semi_automaton (INTERVAL_SET (SUC i0) (SUC s0))
              (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0))
              (XP_AND
                (XP_EQUIV
                    (XP_NEXT_PROP (SUC s0),
                    XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),A.R)))) SUBSET (INTERVAL_SET 0 (SUC s0))` THEN1 (
    SIMP_ALL_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF,
      symbolic_semi_automaton_REWRITES, P_USED_VARS_EVAL, XP_USED_VARS_EVAL, SUBSET_DEF, IN_INTERVAL_SET, IN_UNION, IN_SING, IN_INSERT] THEN
    REPEAT STRIP_TAC THEN (
      RES_TAC THEN
      ASM_SIMP_TAC arith_ss []
    )
  ) THEN

  REPEAT STRIP_TAC THENL [
    REWRITE_TAC[FINITE_INTERVAL_SET],
    ASM_SIMP_TAC std_ss [P_USED_VARS_def, SUBSET_DEF, IN_INTERVAL_SET, IN_SING],

    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC SET_BINARY_ENCODING_SHIFT___INJ THEN
    ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET, FINITE_INTERVAL_SET],


    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC SET_BINARY_ENCODING_SHIFT___INJ THEN
    ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET, FINITE_INTERVAL_SET],


    MATCH_MP_TAC DISJOINT_SUBSET THEN
    Q_TAC EXISTS_TAC `INTERVAL_SET (0) (SUC s0)` THEN
    ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM,
      DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN
    PROVE_TAC[],



    MATCH_MP_TAC DISJOINT_SUBSET THEN
    Q_TAC EXISTS_TAC `INTERVAL_SET (0) (SUC s0)` THEN
    ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM,
      DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN
    REPEAT WEAKEN_HD_TAC THEN
    GEN_TAC THEN
    RIGHT_DISJ_TAC THEN
    SIMP_ALL_TAC std_ss [] THEN
    WEAKEN_NO_TAC 1 THEN
    DECIDE_TAC,


    ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM,
      DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN
    REPEAT WEAKEN_HD_TAC THEN
    GEN_TAC THEN
    `?a:num. 2 ** SUC (s0 - i0) = a` by PROVE_TAC[] THEN
    ASM_REWRITE_TAC[] THEN
    SUBGOAL_TAC `~(a = 0)` THEN1 (
      GSYM_NO_TAC 0 THEN
      ASM_SIMP_TAC std_ss [EXP_EQ_0]
    ) THEN
    WEAKEN_NO_TAC 1 THEN
    DECIDE_TAC
  ]
) THEN
SIMP_ALL_TAC std_ss [FORALL_AND_THM] THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN


SUBGOAL_TAC `!A i (p:num prop_logic). ~(A_SEM i (A_NDET (A, ACCEPT_COND_FG p))) =
                     A_SEM i (A_UNIV (A, ACCEPT_COND_GF (P_NOT p)))` THEN1 (
  REPEAT WEAKEN_HD_TAC THEN
  SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_GF_def, ACCEPT_COND_SEM_def,
    ACCEPT_COND_SEM_TIME_def, ACCEPT_COND_FG_def, ACCEPT_F_def, P_SEM_def] THEN
  METIS_TAC[]
) THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN


SIMP_TAC std_ss [ACCEPT_COND_GF_def] THEN
Q.MATCH_ABBREV_TAC `LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE B) l' =
!i. A_SEM i (A_UNIV (B, ACCEPT_COND ac')) = LTL_SEM i (PSL_TO_LTL psl)` THEN

ASSUME_TAC (INST_TYPE [alpha |-> num] A_UNIV___LTL_KS_SEM___THM) THEN
Q_SPECL_NO_ASSUM 0 [`B`, `ac'`, `PSL_TO_LTL psl`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  REPEAT STRIP_TAC THENL [
    PROVE_TAC[],

    Q.UNABBREV_TAC `B` THEN
    ASM_SIMP_TAC std_ss [SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def,
      symbolic_semi_automaton_REWRITES,
      SET_BINARY_ENCODING_SHIFT___IMAGE_THM,
      PSL_TO_LTL_def,
      RLTL_USED_VARS___PSL_TO_RLTL,
      LTL_USED_VARS___RLTL_TO_LTL,
      P_USED_VARS_EVAL, UNION_EMPTY] THEN
    SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET,
      DISJOINT_DISJ_THM] THEN
    GEN_TAC THEN
    LEFT_DISJ_TAC THEN
    `x <= i0` by PROVE_TAC[] THEN
    ASM_SIMP_TAC arith_ss []
  ]
) THEN

ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN
Q.UNABBREV_TAC `l'` THEN
Q.UNABBREV_TAC `ac'` THEN

MATCH_MP_TAC (prove (``LTL_EQUIVALENT l1 l2 ==> (LTL_KS_SEM M l1 = LTL_KS_SEM M l2)``,
  SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_KS_SEM_def, LTL_SEM_def])) THEN
SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_EQUIV_SEM] THEN
REPEAT GEN_TAC THEN
MATCH_MP_TAC (prove (``(A = B) ==> ((A = x) = (B = x))``, PROVE_TAC[])) THEN
SIMP_TAC std_ss [ACCEPT_COND_TO_LTL_def, LTL_SEM_THM, ACCEPT_F_def, P_SEM_def]
);


val PROBLEM_TO_LTL_KS_SEM___TOTAL =
  store_thm ("PROBLEM_TO_LTL_KS_SEM___TOTAL",
    ``!A p psl i0 s0 f. (F_CLOCK_SERE_FREE psl /\
            IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A /\
           ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION
             F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\
           (A.S = (INTERVAL_SET (SUC i0) s0)) /\
           (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\
           (i0 <= s0) /\
           (f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC s0))) ==>

            ((LTL_KS_SEM
                  (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE
                   (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f))
                  (LTL_EQUIV (LTL_ALWAYS (LTL_PROP (
                      (P_FORALL (SET_TO_LIST A.S)
                       (P_IMPL (VAR_RENAMING_HASHTABLE A.S f,p))))),
                             PSL_TO_LTL psl))

      )  =

      (!K.
      ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) =
       UF_KS_SEM K psl)))``,



REPEAT STRIP_TAC THEN
ASM_SIMP_TAC std_ss [PSL_TO_LTL___UF_KS_SEM] THEN

ASSUME_TAC (INST_TYPE [alpha |-> num] IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS) THEN
Q_SPECL_NO_ASSUM 0 [`A`,  `p`, `(PSL_TO_LTL psl)`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  ASM_REWRITE_TAC[FINITE_INTERVAL_SET,
  INFINITE_UNIV] THEN
  Q_TAC EXISTS_TAC `SUC` THEN
  SIMP_TAC arith_ss [] THEN
  EXISTS_TAC ``0:num`` THEN
  SIMP_TAC arith_ss []
) THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN


SUBGOAL_TAC `DISJOINT (IMAGE f (POW A.S))
                      (SEMI_AUTOMATON_USED_VARS A UNION P_USED_VARS p)` THEN1 (
  ASM_REWRITE_TAC[DISJOINT_DISJ_THM] THEN
  Cases_on `i0 = s0` THENL [
    SUBGOAL_TAC `INTERVAL_SET (SUC i0) s0 = EMPTY` THEN1 (
      ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY]
    ) THEN
    ASM_REWRITE_TAC[IN_IMAGE, IN_POW,
      SUBSET_EMPTY] THEN

    SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def,
                      SET_BINARY_ENCODING_def,
                      IMAGE_EMPTY,
                      SUM_IMAGE_THM] THEN
    FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION,
      SUBSET_DEF, IN_INTERVAL_SET, SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF,
      NOT_IN_EMPTY] THEN
    `~(SUC s0 <= s0)` by DECIDE_TAC THEN
    METIS_TAC[],

    `SUC i0 <= s0` by DECIDE_TAC THEN
    ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM,
      DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN
    FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION,
      SUBSET_DEF, IN_INTERVAL_SET, SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF,
      NOT_IN_EMPTY] THEN
    GEN_TAC THEN
    `~(SUC s0 <= s0)` by DECIDE_TAC THEN
    Cases_on `x <= s0` THEN1 ASM_SIMP_TAC std_ss [] THEN
    `~(x <= i0)` by DECIDE_TAC THEN
    METIS_TAC[]
  ]
) THEN

ASSUME_TAC (INST_TYPE [alpha |-> num] SYMBOLIC___TOTAL_UNIV_G___TO___DET_G___CONCRETE_THM) THEN
Q_SPECL_NO_ASSUM 0 [`A`, `p`, `f`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  ASM_REWRITE_TAC[FINITE_INTERVAL_SET] THEN
  MATCH_MP_TAC SET_BINARY_ENCODING_SHIFT___INJ THEN
  ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET, FINITE_INTERVAL_SET]
) THEN
SIMP_ALL_TAC std_ss [FORALL_AND_THM] THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN



SIMP_TAC std_ss [ACCEPT_COND_G_def] THEN
Q.MATCH_ABBREV_TAC `LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE B) l' =
!i. A_SEM i (A_UNIV (B, ACCEPT_COND ac')) = LTL_SEM i (PSL_TO_LTL psl)` THEN

ASSUME_TAC (INST_TYPE [alpha |-> num] A_UNIV___LTL_KS_SEM___THM) THEN
Q_SPECL_NO_ASSUM 0 [`B`, `ac'`, `PSL_TO_LTL psl`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  REPEAT STRIP_TAC THENL [
    PROVE_TAC[],

    Q.UNABBREV_TAC `B` THEN
    ASM_SIMP_TAC std_ss [RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def,
      symbolic_semi_automaton_REWRITES,
      PSL_TO_LTL_def,
      RLTL_USED_VARS___PSL_TO_RLTL,
      LTL_USED_VARS___RLTL_TO_LTL,
      P_USED_VARS_EVAL, UNION_EMPTY] THEN
    SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET,
      DISJOINT_DISJ_THM] THEN
    GEN_TAC THEN
    LEFT_DISJ_TAC THEN
    `x <= i0` by PROVE_TAC[] THEN

    Cases_on `i0 = s0` THENL [
      SUBGOAL_TAC `INTERVAL_SET (SUC i0) s0 = EMPTY` THEN1 (
        ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY]
      ) THEN
      ASM_REWRITE_TAC[IN_IMAGE, IN_POW,
        SUBSET_EMPTY] THEN

      SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def,
                        SET_BINARY_ENCODING_def,
                        IMAGE_EMPTY,
                        SUM_IMAGE_THM] THEN
      DECIDE_TAC,

      `SUC i0 <= s0` by DECIDE_TAC THEN
      ASM_SIMP_TAC arith_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, IN_INTERVAL_SET]
    ]
  ]
) THEN

ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN
Q.UNABBREV_TAC `l'` THEN
Q.UNABBREV_TAC `ac'` THEN
SIMP_TAC std_ss [ACCEPT_COND_TO_LTL_def]
);













val P_EXISTS___SET_TO_LIST___INTERVAL_SET =
  store_thm ("P_EXISTS___SET_TO_LIST___INTERVAL_SET",
    ``(!n1 n2 p. PROP_LOGIC_EQUIVALENT (P_EXISTS (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (P_EXISTS (INTERVAL_LIST n1 n2) p))``,

    SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, P_EXISTS_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST]
  )

val P_FORALL___SET_TO_LIST___INTERVAL_SET =
  store_thm ("P_FORALL___SET_TO_LIST___INTERVAL_SET",
    ``(!n1 n2 p. PROP_LOGIC_EQUIVALENT (P_FORALL (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (P_FORALL (INTERVAL_LIST n1 n2) p))``,

    SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, P_FORALL_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST]
  )


val P_BIGOR___SET_TO_LIST___INTERVAL_SET =
  store_thm ("P_BIGOR___SET_TO_LIST___INTERVAL_SET",
    ``!n1 n2 f. (PROP_LOGIC_EQUIVALENT
                 (P_BIGOR (SET_TO_LIST (IMAGE f
                    (INTERVAL_SET n1 n2))))
                 (P_BIGOR (MAP f
                    (INTERVAL_LIST n1 n2))))``,

    REPEAT STRIP_TAC THEN
    ASM_SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, P_BIGOR_SEM,
      MEM_MAP, GSYM LEFT_EXISTS_AND_THM, MEM_INTERVAL_LIST,
      MEM_SET_TO_LIST, IMAGE_FINITE, FINITE_INTERVAL_SET,
      IN_IMAGE, IN_INTERVAL_SET]
  )


val XP_BIGOR___SET_TO_LIST___INTERVAL_SET =
  store_thm ("XP_BIGOR___SET_TO_LIST___INTERVAL_SET",
    ``!n1 n2 f. (XPROP_LOGIC_EQUIVALENT
                 (XP_BIGOR (SET_TO_LIST (IMAGE f
                    (INTERVAL_SET n1 n2))))
                 (XP_BIGOR (MAP f
                    (INTERVAL_LIST n1 n2))))``,

    REPEAT STRIP_TAC THEN
    ASM_SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_BIGOR_SEM,
      MEM_MAP, GSYM LEFT_EXISTS_AND_THM, MEM_INTERVAL_LIST,
      MEM_SET_TO_LIST, IMAGE_FINITE, FINITE_INTERVAL_SET,
      IN_IMAGE, IN_INTERVAL_SET]
  )


val XP_NEXT_EXISTS___SET_TO_LIST___INTERVAL_SET =
  store_thm ("XP_NEXT_EXISTS___SET_TO_LIST___INTERVAL_SET",
    ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_NEXT_EXISTS (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_NEXT_EXISTS (INTERVAL_LIST n1 n2) p)``,

    SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_NEXT_EXISTS_SEM,
      SET_TO_LIST_INV, FINITE_INTERVAL_SET,
      LIST_TO_SET___INTERVAL_LIST]);


val XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET =
  store_thm ("XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET",
    ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_CURRENT_EXISTS (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_CURRENT_EXISTS (INTERVAL_LIST n1 n2) p)``,

    SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_CURRENT_EXISTS_SEM,
      SET_TO_LIST_INV, FINITE_INTERVAL_SET,
      LIST_TO_SET___INTERVAL_LIST]);


val XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET =
  store_thm ("XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET",
    ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_NEXT_FORALL (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_NEXT_FORALL (INTERVAL_LIST n1 n2) p)``,

    SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_NEXT_FORALL_SEM,
      SET_TO_LIST_INV, FINITE_INTERVAL_SET,
      LIST_TO_SET___INTERVAL_LIST]);


val XP_CURRENT_FORALL___SET_TO_LIST___INTERVAL_SET =
  store_thm ("XP_CURRENT_FORALL___SET_TO_LIST___INTERVAL_SET",
    ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_CURRENT_FORALL (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_CURRENT_FORALL (INTERVAL_LIST n1 n2) p)``,

    SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_CURRENT_FORALL_SEM,
      SET_TO_LIST_INV, FINITE_INTERVAL_SET,
      LIST_TO_SET___INTERVAL_LIST]);




val IS_EMPTY_FAIR_KRIPKE_STRUCTURE_cong =
  store_thm ("IS_EMPTY_FAIR_KRIPKE_STRUCTURE_cong",

  ``!S0 S0' R R' FC FC'. (
    PROP_LOGIC_EQUIVALENT S0 S0' ==>
    XPROP_LOGIC_EQUIVALENT R R' ==>
    (FC = FC') ==>
    ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0 R) FC) =
    (IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0' R') FC')))``,

  SIMP_TAC std_ss [IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def,
                   PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES,
                   symbolic_kripke_structure_REWRITES,
                   PROP_LOGIC_EQUIVALENT_def,
                   XPROP_LOGIC_EQUIVALENT_def]);



val ks_congset =
  mk_congset ([merge_cs [
  (CSFRAG
   {rewrs  = [],
    relations = [],
    dprocs = [],
    congs  = [IS_EMPTY_FAIR_KRIPKE_STRUCTURE_cong]}),
  xprop_logic_CS, prop_logic_CS]]);









val XP_COND___XP_NEXT_FORALL___REWRITE =
  store_thm ("XP_COND___XP_NEXT_FORALL___REWRITE",
    ``!c l p1 p2.  DISJOINT (XP_USED_X_VARS c) (LIST_TO_SET l) ==> (
      XPROP_LOGIC_EQUIVALENT (XP_COND (c, XP_NEXT_FORALL l p1,  XP_NEXT_FORALL l p2)) (XP_NEXT_FORALL l (XP_COND (c, p1,p2))))``,

    REPEAT STRIP_TAC THEN
    SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_SEM_THM,
      XP_NEXT_FORALL_SEM] THEN
    REPEAT GEN_TAC THEN
    SUBGOAL_TAC `!l'. l' SUBSET LIST_TO_SET l ==>
                      (XP_SEM c (s1,s2 DIFF LIST_TO_SET l UNION l') =
                       XP_SEM c (s1,s2))` THEN1 (
      REPEAT STRIP_TAC THEN
      ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN
      AP_TERM_TAC THEN SIMP_TAC std_ss [] THEN

      ONCE_REWRITE_TAC[EXTENSION] THEN
      SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, SUBSET_DEF, IN_INTER, IN_DIFF,
        IN_UNION] THEN
      PROVE_TAC[]
    ) THEN
    ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN
    METIS_TAC[]);


val XP_COND___XP_CURRENT_EXISTS___REWRITE =
  store_thm ("XP_COND___XP_CURRENT_EXISTS___REWRITE",
    ``!c l p1 p2.  DISJOINT (XP_USED_CURRENT_VARS c) (LIST_TO_SET l) ==> (
      XPROP_LOGIC_EQUIVALENT (XP_COND (c, XP_CURRENT_EXISTS l p1,  XP_CURRENT_EXISTS l p2)) (XP_CURRENT_EXISTS l (XP_COND (c, p1,p2))))``,

    REPEAT STRIP_TAC THEN
    SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_SEM_THM,
      XP_CURRENT_EXISTS_SEM] THEN
    REPEAT GEN_TAC THEN
    SUBGOAL_TAC `!l'. l' SUBSET LIST_TO_SET l ==>
                      (XP_SEM c (s1 DIFF LIST_TO_SET l UNION l', s2) =
                       XP_SEM c (s1,s2))` THEN1 (
      REPEAT STRIP_TAC THEN
      ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN
      AP_TERM_TAC THEN SIMP_TAC std_ss [] THEN

      ONCE_REWRITE_TAC[EXTENSION] THEN
      SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, SUBSET_DEF, IN_INTER, IN_DIFF,
        IN_UNION] THEN
      PROVE_TAC[]
    ) THEN
    METIS_TAC[]);




val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def =
Define
  `(VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING [] n n0 = P_PROP n) /\
   (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (e::l) n n0 =
      P_OR (P_AND (P_PROP e, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l ((2**(e-n0)) + n) n0),
            P_AND (P_NOT (P_PROP e), VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l n n0)))`;

val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___CLEAN_OFFSET =
  store_thm ("VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___CLEAN_OFFSET",
   ``!l n n0 m:num d. ((d <= n) /\ (d >= m) /\ (!e. MEM e l ==> e < m)) ==>
          (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l n n0 =
            (P_VAR_RENAMING (\x. if (x >= m) then x + (n-d) else x)) (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l d n0))``,

     Induct_on `l` THENL [
        SIMP_TAC list_ss [VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def,
         P_VAR_RENAMING_EVAL],

        SIMP_TAC list_ss [VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def,
         P_VAR_RENAMING_EVAL, P_OR_def, prop_logic_11] THEN
        REPEAT GEN_TAC THEN STRIP_TAC THEN
        `h < m` by PROVE_TAC[] THEN
        ASM_SIMP_TAC arith_ss [] THEN
        REPEAT STRIP_TAC THENL [
          Q_SPECL_NO_ASSUM 4 [`n + (2:num) ** (h - n0)`, `n0`, `m`, `d + (2:num) ** (h - n0)`] THEN
          PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC arith_ss [] THEN
          FULL_SIMP_TAC arith_ss [],



          Q_SPECL_NO_ASSUM 4 [`n`, `n0`, `m`, `d`] THEN
          PROVE_CONDITION_NO_ASSUM 0 THEN ASM_SIMP_TAC std_ss [] THEN
          FULL_SIMP_TAC arith_ss []
        ]
      ]);


val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST =
  store_thm ("VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST",
  ``!n1 n2 n3 n4. (n3 <= n1) ==> (VAR_RENAMING_HASHTABLE_LIST (INTERVAL_LIST n1 n2) {} (SET_BINARY_ENCODING_SHIFT n3 n4) = VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST n1 n2) n4 n3)``,

  NTAC 2 GEN_TAC THEN
  Cases_on `n2 < n1` THENL [
    ASM_SIMP_TAC std_ss [INTERVAL_LIST_THM, VAR_RENAMING_HASHTABLE_LIST_def, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def,
    SET_BINARY_ENCODING_SHIFT_def, IMAGE_EMPTY,
    SET_BINARY_ENCODING_def, SUM_IMAGE_THM],

    Induct_on `n2 - n1` THENL [
      REPEAT STRIP_TAC THEN
      `n2 = n1` by DECIDE_TAC THEN
      NTAC 2 (WEAKEN_NO_TAC 2) THEN
      ASM_SIMP_TAC std_ss [INTERVAL_LIST_THM,
        VAR_RENAMING_HASHTABLE_LIST_def,
        VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def,
        SET_BINARY_ENCODING_SHIFT_def,
        IMAGE_SING, SET_BINARY_ENCODING_def,
        SUM_IMAGE_SING, IMAGE_EMPTY,
        SUM_IMAGE_THM],


      REPEAT STRIP_TAC THEN
      `INTERVAL_LIST n1 n2 = n1::INTERVAL_LIST (SUC n1) n2` by
        ASM_SIMP_TAC arith_ss [INTERVAL_LIST_THM] THEN
      ASM_SIMP_TAC std_ss [VAR_RENAMING_HASHTABLE_LIST_def,
        VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, P_OR_def,
        prop_logic_11] THEN
      REPEAT STRIP_TAC THENL [
        ONCE_REWRITE_TAC[VAR_RENAMING_HASHTABLE_LIST___CLEAN_VAR_SET] THEN

        REMAINS_TAC `!x. (x SUBSET {} UNION (LIST_TO_SET (INTERVAL_LIST (SUC n1) n2))) ==>
          ((\x. SET_BINARY_ENCODING_SHIFT n3 n4 (x UNION {n1})) x = SET_BINARY_ENCODING_SHIFT n3 (2**(n1 - n3) + n4) x)` THEN1 (

          ASSUME_TAC (INST_TYPE [alpha  |-> num] VAR_RENAMING_HASHTABLE_LIST___FUN_RESTRICT) THEN

          Q_SPECL_NO_ASSUM 0 [`INTERVAL_LIST (SUC n1) n2`, `EMPTY:num set`, `\x. SET_BINARY_ENCODING_SHIFT n3 n4 (x UNION {n1})`, `SET_BINARY_ENCODING_SHIFT n3 (2**(n1 - n3) + n4)`] THEN
          PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN

          ASM_REWRITE_TAC[] THEN
          Q_SPECL_NO_ASSUM 6 [`n2`, `SUC n1`] THEN
          PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN
          PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN
          Q_SPECL_NO_ASSUM 0 [`n3`, `(2 ** (n1 - n3) + n4)`] THEN
          PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN
          ASM_REWRITE_TAC[]
        ) THEN


        SIMP_TAC std_ss [UNION_EMPTY, LIST_TO_SET___INTERVAL_LIST] THEN
        REPEAT STRIP_TAC THEN
        `FINITE x` by PROVE_TAC[FINITE_INTERVAL_SET, SUBSET_FINITE] THEN
        SUBGOAL_TAC `~(n1 IN x)` THEN1 (
          SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_INTERVAL_SET] THEN
          `~(SUC n1 <= n1)` by DECIDE_TAC THEN
          PROVE_TAC[]
        ) THEN
        ASM_SIMP_TAC arith_ss [FUN_EQ_THM, UNION_SING,
          SET_BINARY_ENCODING_SHIFT_def,
          IMAGE_INSERT, SET_BINARY_ENCODING_def, SUM_IMAGE_THM,
          IMAGE_FINITE] THEN

        AP_TERM_TAC THEN
        SIMP_TAC std_ss [EXTENSION, IN_IMAGE, IN_DELETE] THEN
        REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [
          PROVE_TAC[],
          PROVE_TAC[],

          `~(n1 = n)` by PROVE_TAC[] THEN
          `n < n3` by DECIDE_TAC THEN

          `n IN INTERVAL_SET (SUC n1) n2` by PROVE_TAC[SUBSET_DEF] THEN
          SIMP_ALL_TAC std_ss [IN_INTERVAL_SET] THEN
          DECIDE_TAC
        ],



        Q_SPECL_NO_ASSUM 4 [`n2`, `SUC n1`] THEN
        PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN
        PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN
        Q_SPECL_NO_ASSUM 0 [`n3`, `n4`] THEN
        PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN
        ASM_REWRITE_TAC[]
      ]
    ]
  ]);




val PROBLEM_TO_KRIPKE_STRUCTURE =
  store_thm ("PROBLEM_TO_KRIPKE_STRUCTURE",
    ``!A p psl i0 s0 DS S0 R l' pf sv a. (F_CLOCK_SERE_FREE psl /\
           ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION
             F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\
           (A.S = (INTERVAL_SET (SUC i0) s0)) /\
           (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\
           (i0 <= s0) /\
           (sv = \n:num. 2 * 2**(SUC s0 - i0) + s0 + 3 + n) /\
           LTL_TO_GEN_BUECHI_DS___SEM DS /\
           (l',a,T,pf) IN DS.B /\
           DS.IV SUBSET INTERVAL_SET 0 (2 * 2**(SUC s0 - i0) + s0 + 2) /\
           LTL_EQUIVALENT_INITIAL
            (LTL_EQUIV
              (LTL_ALWAYS
                  (LTL_EVENTUAL
                    (LTL_PROP
                        (P_NOT
                          (P_BIGOR
                              (MAP (\p. P_PROP p)
                                (INTERVAL_LIST
                                    (SUC (SUC s0) + 2 ** SUC (s0 - i0))
                                    (SUC (SUC s0) + 2 ** SUC (s0 - i0) +
                                    PRE (2 ** SUC (s0 - i0))))))))), PSL_TO_LTL psl)) l' /\

          (PROP_LOGIC_EQUIVALENT (P_AND
            (P_FORALL (INTERVAL_LIST (SUC i0) (SUC s0))
               (P_EQUIV
                  (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0),
                   VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                     (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0))
                     (SUC i0))),
             P_AND
               (P_NOT
                  (P_BIGOR
                     (MAP P_PROP
                        (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0))
                           (PRE (2 ** SUC (s0 - i0)) +
                            (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))),
                P_AND
                  (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv,
                   P_NOT (pf sv))))) S0) /\

          (XPROP_LOGIC_EQUIVALENT
          (XP_AND
            (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0))
               (XP_EQUIV
                  (XP_NEXT
                     (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                        (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0))
                        (SUC i0)),
                   XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0))
                     (XP_AND
                        (XP_EQUIV
                           (XP_NEXT_PROP (SUC s0),
                            XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),
                         XP_AND
                           (A.R,
                            XP_CURRENT
                              (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                                 (INTERVAL_LIST (SUC i0) (SUC s0))
                                 (SUC (SUC s0)) (SUC i0))))))),
             XP_AND
               (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0))
                  (XP_EQUIV
                     (XP_NEXT
                        (P_VAR_RENAMING
                           (\n.
                              (if n >= SUC (SUC s0) then
                                 n + (2:num) ** SUC (s0 - i0)
                               else
                                 n))
                           (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                              (INTERVAL_LIST (SUC i0) (SUC s0))
                              (SUC (SUC s0)) (SUC i0))),
                      XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0))
                        (XP_AND
                           (XP_EQUIV
                              (XP_NEXT_PROP (SUC s0),
                               XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),
                            XP_AND
                              (A.R,
                               XP_AND
                                 (XP_NEXT (P_PROP (SUC s0)),
                                  XP_COND
                                    (XP_BIGOR
                                       (MAP XP_PROP
                                          (INTERVAL_LIST
                                             (SUC (SUC s0) +
                                              2 ** SUC (s0 - i0))
                                             (PRE (2 ** SUC (s0 - i0)) +
                                              (SUC (SUC s0) +
                                               2 ** SUC (s0 - i0))))),
                                     XP_CURRENT
                                       (P_VAR_RENAMING
                                          (\n.
                                             (if n >= SUC (SUC s0) then
                                                n + 2 ** SUC (s0 - i0)
                                              else
                                                n))
                                          (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                                             (INTERVAL_LIST (SUC i0)
                                                (SUC s0)) (SUC (SUC s0))
                                             (SUC i0))),
                                     XP_CURRENT
                                       (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                                          (INTERVAL_LIST (SUC i0) (SUC s0))
                                          (SUC (SUC s0)) (SUC i0))))))))),
                          XP_BIGAND (MAP (\xp. xp sv) DS.R)))) R)
      )  ==>

      ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE
          (symbolic_kripke_structure S0 R) (MAP (\x. x sv) DS.FC))
        =

      (!K.
      ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) =
      UF_KS_SEM K psl)))``,


REPEAT STRIP_TAC THEN

`?f. f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)))` by METIS_TAC[] THEN
`?f'. f' = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)) +  2**(SUC(s0-i0)))` by METIS_TAC[] THEN

ASSUME_TAC (GSYM PROBLEM_TO_LTL_KS_SEM) THEN
Q_SPECL_NO_ASSUM 0 [`A`, `p`, `psl`, `i0`, `s0`, `f`, `f'`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC std_ss [] THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN


MATCH_MP_TAC (prove (``!M X f f'. (LTL_EQUIVALENT_INITIAL f f' /\
                      (X = LTL_KS_SEM M f)) ==> (X = LTL_KS_SEM M f')``,
  SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def, LTL_KS_SEM_def] THEN
  PROVE_TAC[])) THEN
Q_TAC EXISTS_TAC `l'` THEN
REPEAT STRIP_TAC THEN1 (

  SUBGOAL_TAC `!S. (IMAGE (\s. P_PROP (f' s)) S) =
                   (IMAGE (\p. P_PROP p) (IMAGE f' S))` THEN1 (
    SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF]
  ) THEN
  UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [] THEN
  DISCH_TAC THEN WEAKEN_HD_TAC THEN
  ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM] THEN

  ASM_CONGRUENCE_SIMP_TAC ltl_cs std_ss [P_BIGOR___SET_TO_LIST___INTERVAL_SET] THEN
  PROVE_TAC[LTL_EQUIVALENT_INITIAL_def]
) THEN
WEAKEN_NO_TAC 4 (*LTL_EQUIVALENT_INITIAL l'*) THEN

GSYM_NO_TAC 7 (*Def sv*) THEN
NTAC 2 (GSYM_NO_TAC 2) (*Def f, f'*) THEN
ASM_SIMP_TAC std_ss [] THEN


Q.MATCH_ABBREV_TAC `IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0 R)
      (MAP (\x. x sv) DS.FC) = LTL_KS_SEM KS l'` THEN
ASSUME_TAC (INST_TYPE [alpha |-> num] LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE) THEN
Q_SPECL_NO_ASSUM 0 [`DS`, `l'`, `pf`, `sv`, `KS`, `a`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  ASM_REWRITE_TAC[] THEN

  SUBGOAL_TAC `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS KS SUBSET
                INTERVAL_SET 0  (2 * 2**(SUC s0 - i0) + s0 + 2)` THEN1 (
    Q.UNABBREV_TAC `KS` THEN
    ASM_SIMP_TAC std_ss [] THEN
    Q.MATCH_ABBREV_TAC `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS
      (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE
          (SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON
            A' f
            f' (P_PROP (SUC s0)))) SUBSET
    INTERVAL_SET 0 (2 * 2 ** (SUC s0 - i0) + s0 + 2)` THEN


    REMAINS_TAC `SEMI_AUTOMATON_USED_VARS ((SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON A' f f'
            (P_PROP (SUC s0)))) SUBSET
            INTERVAL_SET 0 (2 * 2 ** (SUC s0 - i0) + s0 + 2)` THEN1 (
      UNDISCH_HD_TAC THEN
      MATCH_MP_TAC (prove (``(C SUBSET A) ==> (A SUBSET B ==> C SUBSET B)``, METIS_TAC[SUBSET_TRANS])) THEN
      SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def,
                        SEMI_AUTOMATON_USED_VARS___DIRECT_DEF,
                        SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def,
                        symbolic_kripke_structure_REWRITES, SUBSET_DEF,
                        IN_UNION]
    ) THEN

    SUBGOAL_TAC `SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)` THEN1 (
      ASM_REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def] THEN
      SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET] THEN
      REPEAT STRIP_TAC THEN
      RES_TAC THEN
      DECIDE_TAC
    ) THEN

    ASSUME_TAC (INST_TYPE [alpha |-> num] SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS) THEN
    Q_SPECL_NO_ASSUM 0 [`A'`, `f`, `f'`, `P_PROP (SUC s0)`] THEN
    PROVE_CONDITION_NO_ASSUM 0 THEN1 (
      Q.UNABBREV_TAC `A'` THEN
      NTAC 2 (GSYM_NO_TAC 2) (*f, f'*) THEN
      ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES,
        FINITE_INTERVAL_SET, SET_BINARY_ENCODING_SHIFT___IMAGE_THM,
        SEMI_AUTOMATON_USED_VARS___DIRECT_DEF,
        P_USED_VARS_EVAL, XP_USED_VARS_EVAL,
        DISJOINT_DISJ_THM] THEN
      SIMP_ALL_TAC std_ss [IN_UNION, SUBSET_DEF, IN_INTERVAL_SET, IN_SING, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN
      REPEAT STRIP_TAC THEN (
        LEFT_DISJ_TAC THEN
        SIMP_ALL_TAC std_ss [] THEN
        RES_TAC THEN
        ASM_SIMP_TAC arith_ss []
      )
    ) THEN

    ASM_REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def,
      SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def,
      symbolic_semi_automaton_REWRITES] THEN
    Q.UNABBREV_TAC `A'` THEN
    NTAC 2 (GSYM_NO_TAC 3) THEN
    ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM,
      symbolic_semi_automaton_REWRITES, SEMI_AUTOMATON_USED_INPUT_VARS_def,
      P_USED_VARS_EVAL, XP_USED_VARS_EVAL] THEN
    `(SUC s0) - i0 = SUC (s0 - i0)` by DECIDE_TAC THEN
    SUBGOAL_TAC `~(2:num ** (s0 - i0) = 0)` THEN1 (
      SIMP_TAC std_ss [EXP_EQ_0]
    ) THEN
    `?a. (2 :num) ** (s0 - i0) = a` by METIS_TAC[] THEN
    FULL_SIMP_TAC std_ss [EXP] THEN
    UNDISCH_NO_TAC 1 (*~a = 0*) THEN
    UNDISCH_NO_TAC 5 (*SEMI_AUTOMATON_USED_VARS*) THEN
    UNDISCH_NO_TAC 12 (*i0 <= s0*) THEN
    UNDISCH_NO_TAC 12 (*P_USED_VARS p *) THEN
    REPEAT WEAKEN_HD_TAC THEN
    SIMP_TAC std_ss [SUBSET_DEF,
      IN_UNION, IN_DIFF, IN_SING, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF,
      IN_INTERVAL_SET, EXP] THEN

    REPEAT STRIP_TAC THEN (
      RES_TAC THEN
      DECIDE_TAC
    )
  ) THEN

  UNDISCH_HD_TAC THEN
  UNDISCH_NO_TAC 9 (*i0 <= s0*) THEN
  UNDISCH_NO_TAC 6 (*DS.IV*) THEN
  GSYM_NO_TAC 3 (*def sv*) THEN
  ASM_SIMP_TAC std_ss [] THEN
  REPEAT WEAKEN_HD_TAC THEN
  SIMP_TAC std_ss [IS_ELEMENT_ITERATOR_def, IN_UNION,
    SUBSET_DEF, IN_INTERVAL_SET] THEN
  REPEAT STRIP_TAC THENL [
    RES_TAC THEN
    DECIDE_TAC,

    RES_TAC THEN
    DECIDE_TAC
  ]
) THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN


Q.UNABBREV_TAC `KS` THEN
NTAC 3 (GSYM_NO_TAC 2) (*Def f, f', sv*) THEN
ASM_SIMP_TAC std_ss [] THEN

SUBGOAL_TAC `!n1 n2 S. (IMAGE (\s. P_PROP (SET_BINARY_ENCODING_SHIFT n1 n2 s)) S) =
  (IMAGE P_PROP (IMAGE (SET_BINARY_ENCODING_SHIFT n1 n2) S))` THEN1 (
  SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF]
) THEN
SUBGOAL_TAC `!n1 n2 S. (IMAGE (\s. XP_PROP (SET_BINARY_ENCODING_SHIFT n1 n2 s)) S) =
  (IMAGE XP_PROP (IMAGE (SET_BINARY_ENCODING_SHIFT n1 n2) S))` THEN1 (
  SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF]
) THEN
ASM_SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def,
  SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def,
  symbolic_semi_automaton_REWRITES,
  symbolic_kripke_structure_REWRITES,
  SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def,
  SET_BINARY_ENCODING_SHIFT___IMAGE_THM] THEN
NTAC 2 WEAKEN_HD_TAC THEN


ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET) THEN
Q_SPEC_NO_ASSUM 0 `INTERVAL_LIST (SUC i0) (SUC s0)` THEN
SIMP_ALL_TAC std_ss [LIST_TO_SET___INTERVAL_LIST] THEN

GSYM_NO_TAC 3 (*sv*) THEN
ASM_SIMP_TAC std_ss [] THEN

ASM_CONGRUENCE_SIMP_TAC ks_congset arith_ss [P_BIGOR___SET_TO_LIST___INTERVAL_SET,
XP_BIGOR___SET_TO_LIST___INTERVAL_SET,
P_FORALL___SET_TO_LIST___INTERVAL_SET,
XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET,
XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET,
VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET,
VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST] THEN

ASSUME_TAC (SIMP_RULE std_ss [RIGHT_FORALL_IMP_THM] (INST_TYPE [alpha |-> num] XP_COND___XP_NEXT_FORALL___REWRITE)) THEN
Q_SPECL_NO_ASSUM 0 [`XP_BIGOR
                  (MAP XP_PROP
                      (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0))
                        (PRE (2 ** SUC (s0 - i0)) +
                          (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))`,
                    `(INTERVAL_LIST (SUC i0) (SUC s0))`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  ASM_SIMP_TAC list_ss [DISJOINT_DISJ_THM, XP_BIGOR___XP_USED_VARS, IN_LIST_BIGUNION,
    MAP_MAP_o, combinTheory.o_DEF, XP_USED_VARS_EVAL, MEM_MAP,
    GSYM LEFT_FORALL_OR_THM, NOT_IN_EMPTY]
) THEN






`?ht. VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                     (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0))
                     (SUC i0) = ht` by METIS_TAC[] THEN
SUBGOAL_TAC `(VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                (INTERVAL_LIST (SUC i0) (SUC s0))
                (SUC (SUC s0) + 2 ** SUC (s0 - i0))
                (SUC i0)) = P_VAR_RENAMING (\n:num. if (n >= (SUC (SUC s0))) then n + 2 ** SUC (s0 - i0) else n) ht` THEN1 (
  GSYM_NO_TAC 0 THEN
  ASM_REWRITE_TAC[] THEN
  ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___CLEAN_OFFSET) THEN
  Q_SPECL_NO_ASSUM 0 [`INTERVAL_LIST (SUC i0) (SUC s0)`, `(SUC (SUC s0) + 2 ** SUC (s0 - i0))`, `(SUC i0)`, `SUC (SUC s0)`, `SUC (SUC s0)`] THEN
  PROVE_CONDITION_NO_ASSUM 0 THEN1 SIMP_TAC arith_ss [MEM_INTERVAL_LIST] THEN

  ASM_REWRITE_TAC[] THEN
  SIMP_TAC arith_ss []
) THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN

ASSUME_TAC (SIMP_RULE std_ss [RIGHT_FORALL_IMP_THM] (INST_TYPE [alpha |-> num] XP_COND___XP_CURRENT_EXISTS___REWRITE)) THEN
Q_SPECL_NO_ASSUM 0 [`XP_BIGOR
                  (MAP XP_PROP
                      (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0))
                        (PRE (2 ** SUC (s0 - i0)) +
                          (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))`,
                    `(INTERVAL_LIST (SUC i0) (SUC s0))`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  ASM_SIMP_TAC list_ss [DISJOINT_DISJ_THM, XP_BIGOR___XP_USED_VARS, IN_LIST_BIGUNION,
    MAP_MAP_o, combinTheory.o_DEF, XP_USED_VARS_EVAL, MEM_MAP,
    GSYM LEFT_FORALL_OR_THM, IN_SING] THEN
  REWRITE_TAC [MEM_INTERVAL_LIST] THEN
  REPEAT WEAKEN_HD_TAC THEN GEN_TAC THEN
  LEFT_DISJ_TAC THEN
  FULL_SIMP_TAC arith_ss []
) THEN

GSYM_NO_TAC 1 THEN
ASM_CONGRUENCE_SIMP_TAC ks_congset arith_ss []
);





val PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL =
  store_thm ("PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL",
    ``!A p psl i0 s0 DS S0 R l' pf sv a. (
            F_CLOCK_SERE_FREE psl /\
            IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A /\
           ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION
             F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\
           (A.S = (INTERVAL_SET (SUC i0) s0)) /\
           (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\
           (i0 <= s0) /\
           (sv = \n:num. 2**(s0 - i0) + s0 + 1 + n) /\
           LTL_TO_GEN_BUECHI_DS___SEM DS /\
           (l',a,T,pf) IN DS.B /\
           DS.IV SUBSET INTERVAL_SET 0 (2**(s0 - i0) + s0) /\
           LTL_EQUIVALENT_INITIAL
            (LTL_EQUIV
              (LTL_ALWAYS
                (LTL_PROP
                  (P_FORALL (INTERVAL_LIST (SUC i0) s0)
                      (P_IMPL
                        (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                          (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0),
                          p)))), PSL_TO_LTL psl)) l' /\

          (PROP_LOGIC_EQUIVALENT  (P_AND
            (P_FORALL (INTERVAL_LIST (SUC i0) s0)
               (P_EQUIV
                  (A.S0,
                   VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                     (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0))),
             P_AND
               (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv,P_NOT (pf sv)))) S0) /\

          (XPROP_LOGIC_EQUIVALENT
           (XP_AND
            (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) s0)
               (XP_EQUIV
                  (XP_NEXT
                     (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                        (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0)),
                   XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) s0)
                     (XP_AND
                        (A.R,
                         XP_CURRENT
                           (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING
                              (INTERVAL_LIST (SUC i0) s0) (SUC s0)
                              (SUC i0)))))),
             XP_BIGAND (MAP (\xp. xp sv) DS.R))) R)
      )  ==>

      ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE
          (symbolic_kripke_structure S0 R) (MAP (\x. x sv) DS.FC))
        =

      (!K.
      ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) =
      UF_KS_SEM K psl)))``,


REPEAT STRIP_TAC THEN

`?f. f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC s0)` by METIS_TAC[] THEN

ASSUME_TAC (GSYM PROBLEM_TO_LTL_KS_SEM___TOTAL) THEN
Q_SPECL_NO_ASSUM 0 [`A`, `p`, `psl`, `i0`, `s0`, `f`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC std_ss [] THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN


MATCH_MP_TAC (prove (``!M X f f'. (LTL_EQUIVALENT_INITIAL f f' /\
                      (X = LTL_KS_SEM M f)) ==> (X = LTL_KS_SEM M f')``,
  SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def, LTL_KS_SEM_def] THEN
  PROVE_TAC[])) THEN
Q_TAC EXISTS_TAC `l'` THEN
REPEAT STRIP_TAC THEN1 (

  FULL_SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def] THEN
  GSYM_NO_TAC 3 THEN
  ASM_SIMP_TAC arith_ss [LTL_SEM_THM, P_FORALL_SEM, LIST_TO_SET___INTERVAL_LIST,
    SET_TO_LIST_INV, FINITE_INTERVAL_SET, P_SEM_THM,
    GSYM VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST,
    GSYM (SIMP_RULE std_ss [PROP_LOGIC_EQUIVALENT_def] VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET)]
) THEN
WEAKEN_NO_TAC 3 (*LTL_EQUIVALENT_INITIAL l'*) THEN

GSYM_NO_TAC 6 (*Def sv*) THEN
GSYM_NO_TAC 1 (*Def f*) THEN
ASM_SIMP_TAC std_ss [] THEN


Q.ABBREV_TAC `KS = (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE
         (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f))` THEN
ASSUME_TAC (INST_TYPE [alpha |-> num] LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE) THEN
Q_SPECL_NO_ASSUM 0 [`DS`, `l'`, `pf`, `sv`, `KS`, `a`] THEN
PROVE_CONDITION_NO_ASSUM 0 THEN1 (
  ASM_REWRITE_TAC[] THEN

  SUBGOAL_TAC `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS KS SUBSET
                INTERVAL_SET 0  (2**(s0 - i0) + s0)` THEN1 (
    Q.UNABBREV_TAC `KS` THEN
    REMAINS_TAC `SEMI_AUTOMATON_USED_VARS (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f) SUBSET  INTERVAL_SET 0 (2 ** (s0 - i0) + s0)` THEN1 (
      UNDISCH_HD_TAC THEN
      MATCH_MP_TAC (prove (``(C SUBSET A) ==> (A SUBSET B ==> C SUBSET B)``, METIS_TAC[SUBSET_TRANS])) THEN
      SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def,
                        SEMI_AUTOMATON_USED_VARS___DIRECT_DEF,
                        SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def,
                        symbolic_kripke_structure_REWRITES, SUBSET_DEF,
                        IN_UNION]
    ) THEN

    SUBGOAL_TAC `SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)` THEN1 (
      ASM_REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def] THEN
      SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET] THEN
      REPEAT STRIP_TAC THEN
      RES_TAC THEN
      DECIDE_TAC
    ) THEN

    ASSUME_TAC (INST_TYPE [alpha |-> num] RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS) THEN
    Q_SPECL_NO_ASSUM 0 [`A`, `f`] THEN
    PROVE_CONDITION_NO_ASSUM 0 THEN1 (
      GSYM_NO_TAC 1 (*Def f*) THEN
      ASM_SIMP_TAC std_ss [FINITE_INTERVAL_SET,
        DISJOINT_DISJ_THM, SEMI_AUTOMATON_USED_VARS_def, IN_UNION] THEN
      GEN_TAC THEN
      LEFT_DISJ_TAC THEN
      SUBGOAL_TAC `x <= s0` THEN1 (
        CLEAN_ASSUMPTIONS_TAC THENL [
          `x IN INTERVAL_SET 0 i0` by METIS_TAC[UNION_SUBSET, SUBSET_DEF] THEN
          FULL_SIMP_TAC arith_ss [IN_INTERVAL_SET],

          FULL_SIMP_TAC arith_ss [IN_INTERVAL_SET]
        ]
      ) THEN

      Cases_on `i0 = s0` THENL [
        SUBGOAL_TAC `INTERVAL_SET (SUC i0) s0 = EMPTY` THEN1 (
          ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY]
        ) THEN
        ASM_REWRITE_TAC[IN_IMAGE, IN_POW,
          SUBSET_EMPTY] THEN

        SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def,
                          SET_BINARY_ENCODING_def,
                          IMAGE_EMPTY,
                          SUM_IMAGE_THM] THEN
        DECIDE_TAC,

        `SUC i0 <= s0` by DECIDE_TAC THEN
        ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM,
          DISJOINT_DISJ_THM, IN_INTERVAL_SET]
      ]
    ) THEN

    ASM_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def,
      RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def,
      symbolic_semi_automaton_REWRITES, UNION_SUBSET, SUBSET_DEF,
      IN_INTERVAL_SET, IN_UNION] THEN
    REPEAT STRIP_TAC THENL [
      `x IN INTERVAL_SET 0 i0` by PROVE_TAC[UNION_SUBSET, SUBSET_DEF] THEN
      UNDISCH_HD_TAC THEN
      ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET],


      UNDISCH_HD_TAC THEN
      GSYM_NO_TAC 2 (*Def f*) THEN
      ASM_REWRITE_TAC[] THEN
      Cases_on `i0 = s0` THENL [
        SUBGOAL_TAC `INTERVAL_SET (SUC s0) s0 = EMPTY` THEN1 (
          ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY]
        ) THEN
        ASM_REWRITE_TAC[IN_IMAGE, IN_POW,
          SUBSET_EMPTY] THEN

        SIMP_TAC arith_ss [SET_BINARY_ENCODING_SHIFT_def,
                          SET_BINARY_ENCODING_def,
                          IMAGE_EMPTY,
                          SUM_IMAGE_THM],

        `SUC i0 <= s0` by DECIDE_TAC THEN
        `SUC (s0 - SUC i0) = (s0 - i0)` by DECIDE_TAC THEN
        ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM,
          DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN
        WEAKEN_HD_TAC THEN
        `~((2:num)**(s0 - i0) = 0)` by SIMP_TAC std_ss [EXP_EQ_0] THEN
        DECIDE_TAC
      ]
    ]
  ) THEN
  GSYM_NO_TAC 3 THEN
  ASM_SIMP_TAC std_ss [IS_ELEMENT_ITERATOR_def, IN_UNION] THEN
  REPEAT STRIP_TAC THEN (
    `2 ** (s0 - i0) + s0 + 1 + i IN INTERVAL_SET 0 (2 ** (s0 - i0) + s0)` by
      METIS_TAC[SUBSET_DEF] THEN
    UNDISCH_HD_TAC THEN
    SIMP_TAC arith_ss [IN_INTERVAL_SET]
  )
) THEN
ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN


Q.UNABBREV_TAC `KS` THEN
NTAC 2 (GSYM_NO_TAC 1) (*Def f, sv*) THEN
ASM_SIMP_TAC std_ss [RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def,
  SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def,
  SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def,
  symbolic_semi_automaton_REWRITES,
  symbolic_kripke_structure_REWRITES] THEN

ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET) THEN
Q_SPEC_NO_ASSUM 0 `INTERVAL_LIST (SUC i0) s0` THEN
SIMP_ALL_TAC std_ss [LIST_TO_SET___INTERVAL_LIST] THEN

GSYM_NO_TAC 2 (*sv*) THEN
ASM_SIMP_TAC std_ss [] THEN

ASM_CONGRUENCE_SIMP_TAC ks_congset arith_ss [P_BIGOR___SET_TO_LIST___INTERVAL_SET,
XP_BIGOR___SET_TO_LIST___INTERVAL_SET,
P_FORALL___SET_TO_LIST___INTERVAL_SET,
XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET,
XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET,
VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET,
VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST]
);



val _ = export_theory();
